;;;============================================================================
;;;
;;; Subject: Representation of degeneracy lists as natural numbers and Kenzo
;;;          definitions 
;;;
;;;----------------------------------------------------------------------------
;;;
;;; FJMM 13-12-08
;;;
;;;============================================================================

#| To certify this book:

(certify-book "dg-natural" 0 nil)

|#

(in-package "ACL2")

(set-verify-guards-eagerness 0)

;;;----------------------------------------------------------------------------

(encapsulate
 ()

 (local
  (defthm commutativity-2-of-+-lemma
    (equal (+ (+ x y) z)
	   (+ (+ y x) z))
     :rule-classes nil))

 (defthm commutativity-2-of-+
    (equal (+ x (+ y z))
	   (+ y (+ x z)))
    :hints (("Goal"
	     :in-theory (disable commutativity-of-+)
	     :use commutativity-2-of-+-lemma))))

;;;============================================================================
;;;
;;; 0) Preliminaries
;;;
;;;============================================================================

#|
(include-book "arithmetic-4/top" :dir :system)

(set-default-hints '((nonlinearp-default-hint stable-under-simplificationp 
					      hist pspv)))
|#

(encapsulate
 ()

 (local
  (include-book "rtl/rel7/support/support/top" :dir :system))

;;;============================================================================
;;;
;;; 0.1) 'ash' properties
;;;
;;;============================================================================

 (defthm natp-+
   (implies (and (natp n1)
		 (natp n2))
	    (natp (+ n1 n2))))
 
 (defthm ash-auxiliar
   (implies (and (natp n)
		 (natp m)
		 (< m (ash 1 n)))
	    (< (+ m (ash 1 n)) (ash 1 (+ 1 n))))
   :hints (("Goal" :in-theory (enable ash expt-split))))
 
 (defthm nat-<-ash
   (implies (and (natp m)
		 (natp n)
		 (< m (ash 1 n)))
	    (< m (ash 1 (+ 1 n))))
   :hints (("Goal" :in-theory (enable ash expt-split))))
 
 (defthm natp-ash-1
   (implies (natp n)
	    (natp (ash n -1))))
 
 (defthm ash-ash
   (implies (and (natp n1)
		 (integerp n2)
		 (natp m))
	    (equal (ash (ash m n1) n2)
		   (ash m (+ n1 n2))))
   :hints (("Goal" :in-theory (enable ash expt-split))))
 
 (defthm natp-ash
   (implies (and (natp n)
		 (natp m))
	    (natp (ash n m)))
   :hints (("Goal" :in-theory (enable ash))))
 
 (defthm natp-ash-0
   (implies (natp n)
	    (equal (ash n 0) n))
   :hints (("Goal" :in-theory (enable ash))))

 (defthm natp-ash+1>0
   (implies (natp n)
	    (<= 0 (ash n 1)))
   :rule-classes :linear)

 (defthm evenp+1
   (implies (evenp n)
	    (not (evenp (+ 1 n))))
   :hints (("Goal" :in-theory (enable evenp))))

 (defthm |(ash n -1) < n|
   (implies (not (zp n))
	    (< (ash n -1) n))
   :hints (("Goal" :in-theory (enable ash)))  
   :rule-classes :linear)

 (defthm evenp-ash-n-1
   (implies (natp n)
	    (evenp (ash n 1)))
   :hints (("Goal" :in-theory (enable evenp ash))))

 (defthm evenp-ash-1-n
   (implies (and (natp n)
                 (< 0 n))
	    (evenp (ash 1 n)))
   :hints (("Goal" :in-theory (enable evenp ash))))

 (defthm natp-evenp-not-zp-ash-1>0
   (implies (and (natp n)
		 (evenp n)
		 (not (zp n)))
	    (< 0 (ash n -1)))
   :hints (("Goal" :in-theory (enable evenp ash)))
   :rule-classes :linear)

 (defthm ash-even
   (implies (and (natp n)
		 (evenp n))
	    (equal (ash (ash n -1) 1) n))
   :hints (("Goal" :in-theory (enable evenp ash))))

 (defthm ash-odd
   (implies (and (natp n)
		 (not (evenp n)))
	    (equal (+ 1 (ash (ash n -1) 1)) n))
   :hints (("Goal" :in-theory (enable evenp ash))))

 (defthm ash-0
   (implies (and (equal (ash n 1) 0)
		 (natp n))
	    (equal n 0))
   :hints (("Goal" :in-theory (enable ash)))  
   :rule-classes :forward-chaining)

 (defthm ash-1--1
   (implies (natp n)
	    (equal (ash (ash n 1) -1)
		   n))
   :hints (("Goal" :in-theory (enable ash))))

 (defthm ash-1-1-1
   (implies (natp n)
	    (equal (ash (+ 1 (ash n 1)) -1)
		   n))
   :hints (("Goal" :in-theory (enable ash))))

 (defthm 1+1+nat
   (implies (natp n)
	    (equal (+ 1 1 n) (+ 2 n))))

 (defthm +-ash-expt
   (implies (and (natp m)
		 (natp n))
	    (equal (+ (ash m 1) (ash 1 (+ 1 n)))
		   (ash (+ m (ash 1 n)) 1)))
   :hints (("Goal" :in-theory (enable evenp ash))))

 (defthm ash-logxor
   (implies (and (natp n1)
		 (natp n2))
	    (equal (ash (logxor n1 n2) 1)
		   (logxor (ash n1 1) (ash n2 1))))
   :hints (("Goal"
	    :in-theory (enable evenp ash
			       logxor logeqv lognot logorc1 logior logand))))

 (defthm ash-logxor+1
   (implies (and (natp n1)
		 (natp n2))
	    (equal (logxor (ash n2 1) (+ 1 (ash n1 1)))
		   (+ 1 (ash (logxor n1 n2) 1))))
   :hints (("Goal"
	    :in-theory (enable evenp ash
			       logxor logeqv lognot logorc1 logior logand))))
 
 (in-theory (disable ash))

;;;============================================================================
;;;
;;; 0.2) 'logxor' properties
;;;
;;;============================================================================

 (defthm natp-logxor
   (implies (and (natp n1)
		 (natp n2))
	    (natp (logxor n1 n2))))

 (defthm logxor-1-even
   (implies (and (evenp n)
		 (natp n))
	    (equal (logxor 1 n) (+ 1 n)))
   :hints (("Goal"
	    :in-theory (enable logxor logeqv logorc1 logior lognot logand
			       expt evenp))))

 (defthm logxor-0-1
   (implies (natp n)
	    (equal (logxor 0 n) n)))

 (defthm logxor-commutativo
   (implies (and (natp n1)
		 (natp n2))
	    (equal (logxor n1 n2)
		   (logxor n2 n1))))
 
 (defthm logxor-asociativo
   (implies (and (natp n1)
		 (natp n2)
		 (natp n3))
	    (equal (logxor (logxor n1 n2) n3)
		   (logxor n1 (logxor n2 n3)))))

 (local
  (defun logcomp (m n)
    (declare (xargs :measure (if (natp n) n 0)
		    :hints (("Goal" :in-theory (disable ash)))))
    (if (and (natp n) (natp m))
	(if (zerop n)
	    (< 0 m)
	    (and (evenp m) (logcomp (ash m -1) (ash n -1))))
	nil)))

 (local
  (defthm logcomp-logxor
    (implies (and (natp n)
		  (natp m)
		  (logcomp m n))
	     (equal (logxor m n) (+ m n)))
    :hints (("Goal" :in-theory (enable ash logxor logeqv logorc1 logior lognot
				       oddp evenp logand)))
    :rule-classes nil))

 (local
  (defun logcomp-<-expt-induct (m n)
    (declare (xargs :measure (if (natp n) n 0)
		    :hints (("Goal" :in-theory (disable ash)))))
    (if (and (natp n) (natp m))
	(if (zerop n)
	    (+ m n)
	    (logcomp-<-expt-induct (ash m -1) (- n 1)))
	nil)))

 (local
  (defthm logcomp-ash--1
    (implies (and (natp n)
		  (natp m)
		  (evenp m)
		  (logcomp (ash m -1) (ash n -1)))
	     (logcomp m n))
    :rule-classes nil))

 (local
  (defthm <-ash--1
    (implies (and (natp m)
		  (natp n)
		  (evenp n))
	     (iff (< (ash m -1) (ash n -1))
	          (< m n)))
    :hints (("Goal" :in-theory (enable evenp ash)))))

 (local
  (defthm logcomp-<-ash-1-n
    (implies (and (natp m)
		  (natp n))
	     (iff (logcomp (ash 1 n) m)
	          (< m (ash 1 n))))
    :hints (("Goal" :induct (logcomp-<-expt-induct m n))
            ("Subgoal *1/2" :use (:instance <-ash--1 (n (ash 1 n)))))))

 (defthm logxor-m-ash-1-n
   (implies (and (natp n)
		 (natp m)
		 (< m (ash 1 n)))
	    (equal (logxor m (ash 1 n))
		   (+ m (ash 1 n))))
   :hints (("Goal"
	    :use (logcomp-<-ash-1-n
		  (:instance logcomp-logxor
			     (m (ash 1 n))
			     (n m))))))
 
 (defthm logxor-ash-ash-1
   (equal (logxor (ash m -1) (ash n -1))
	  (ash (logxor m n) -1))
   :hints (("Goal" :in-theory (enable ash logxor logeqv logorc1 logior lognot
				      oddp evenp logand))))

 (local
  (defthm logcomp-m-logxor
    (implies (and (logcomp m n1)
		  (logcomp m n2))
	     (logcomp m (logxor n1 n2)))))
 
 (defthm logxor-<-expt
   (implies (and (natp m1)
		 (natp m2)
		 (natp n)
		 (< m1 (ash 1 n))
		 (< m2 (ash 1 n)))
	    (< (logxor m1 m2) (ash 1 n)))
   :hints (("Goal" :in-theory (disable logcomp-m-logxor)
	    :use (:instance logcomp-m-logxor
			    (m (ash 1 n))
			    (n1 m1)
			    (n2 m2)))))
 
 )

(in-theory (disable ash logxor evenp natp))

;;;============================================================================
;;;
;;; 2) Transformation functions
;;;
;;;============================================================================

;; (0 1 0 1 1 0 1) -> 90
;;    ^   ^ ^   ^
;;    2   8 16 64

; (defun dgb->dgn (dgb)
;   (if (endp dgb)
;       0
;       (+ (car dgb) (ash (dgb->dgn (cdr dgb)) 1))))

(defun dgb->dgn (dgb)
  (cond ((endp dgb) 0)
	(t (+ (car dgb) (ash (dgb->dgn (cdr dgb)) 1)))))

; (dgb->dgn '(0 1 0 1 1 0 1)) -> 90
; (dgb->dgn '(1 1 0 1 0 1))   -> 43
; (dgb->dgn '())              -> 0

;;;----------------------------------------------------------------------------

; (defun dgn->dgb (dgn)
;   (declare (xargs :measure (if (zp dgn) 0 dgn)))
;   (if (zp dgn)
;       nil
;       (cons (if (evenp dgn) 0 1)
; 	    (dgn->dgb (ash dgn -1)))))

(defun dgn->dgb (dgn)
  (declare (xargs :measure (if (zp dgn) 0 dgn)))
  (cond ((zp dgn) nil)
	(t (cons (if (evenp dgn) 0 1)
		 (dgn->dgb (ash dgn -1))))))

; (dgn->dgb 90) -> (0 1 0 1 1 0 1)
; (dgn->dgb 43) -> (1 1 0 1 0 1)
; (dgn->dgb 0)  -> nil

;;;============================================================================
;;;
;;; 3) Properties
;;;
;;;============================================================================

(include-book "dg-binary")

;;;----------------------------------------------------------------------------
;;;
;;; 3.1) Domain properties
;;;
;;;----------------------------------------------------------------------------

(defthm natp-dgb->dgn
  (implies (dgb-p dgb)
	   (natp (dgb->dgn dgb))))

;;;----------------------------------------------------------------------------

(defthm consp-dgn->dgb
  (implies (and (natp dgn)
		(< 0 dgn))
	   (consp (dgn->dgb dgn))))

(defthm dgb-p-dgn->dgb
  (implies (natp dgn)
	   (dgb-p (dgn->dgb dgn))))
;  :hints (("Goal" :induct (dgn->dgb dgn))))

;;;----------------------------------------------------------------------------
;;;
;;; 3.2) Composition of transformations
;;;
;;;----------------------------------------------------------------------------

(defthm dgb->dgn-dgn->dgb
  (implies (natp dgn)
	   (equal (dgb->dgn (dgn->dgb dgn))
		  dgn)))
;  :hints (("Goal" :induct (dgn->dgb dgn))))

;;;----------------------------------------------------------------------------

(defthm dgn->dgb-dgb->dgn
  (implies (dgb-p dgb)
	   (equal (dgn->dgb (dgb->dgn dgb))
		  dgb))
  :hints (("Goal" :in-theory (disable evenp))
	  ("Subgoal *1/5.3"
	   :use (:instance ash-0 (n (dgb->dgn (cdr dgb)))))))

;;;============================================================================
;;;
;;; 4) Kenzo definitions and properties
;;;
;;;============================================================================

(defun dgop*dgop-loop (dgop1 dgop2 dgop bmark)
  (declare (xargs :guard (and (natp dgop1)
			      (natp dgop2)
			      (natp dgop)
			      (natp bmark))
		  :measure (if (natp dgop1) dgop1 0)
		  :hints (("Goal" :in-theory (disable ash)))))
  (if (and (natp dgop1)
           (natp dgop2))
      (cond ((zerop dgop1)
             (logxor dgop (ash dgop2 bmark)))
            ((zerop dgop2)
             (logxor dgop (ash dgop1 bmark)))
            ((evenp dgop1)
             (dgop*dgop-loop (ash dgop1 -1) (ash dgop2 -1)
                             (if (oddp dgop2) 
                                 (+ dgop (ash 1 bmark)) 
                                 dgop)
                             (+ bmark 1)))
            (t (dgop*dgop-loop (ash dgop1 -1) dgop2
                               (+ dgop (ash 1 bmark)) (+ bmark 1))))
      0))

(verify-guards dgop*dgop-loop)

(defun dgop*dgop (dgop1 dgop2)
  (declare (xargs :guard (and (natp dgop1)
			      (natp dgop2))))
  (dgop*dgop-loop dgop1 dgop2 0 0))

(verify-guards dgop*dgop)

;;;----------------------------------------------------------------------------

(defthm natp-dgop*dgop-loop
  (implies (and (natp dgn1)
		(natp dgn2)
		(natp dgn)
		(natp n)
		(< dgn (ash 1 n)))
	   (natp (dgop*dgop-loop dgn1 dgn2 dgn n)))
  :hints (("Goal" :in-theory (disable ash logxor natp evenp))))

(defthm dgop*dgop-loop-0
  (implies (natp dgn)
	   (equal (dgop*dgop-loop dgn 0 0 0) dgn)))

(defthm dgop*dgop-0-1
  (implies (natp dgn)
	   (equal (dgop*dgop 0 dgn) dgn)))

(defthm dgop*dgop-0-2
  (implies (natp dgn)
	   (equal (dgop*dgop dgn 0) dgn)))

(defthm dgop*dgop-1-1
  (implies (natp dgn)
	   (equal (dgop*dgop 1 dgn)
		  (+ 1 (ash dgn 1)))))

(defthm dgop*dgop-even-1
  (implies (and (natp dgn)
		(evenp dgn))
	   (equal (dgop*dgop dgn 1)
		  (+ 1 dgn))))

(defthm dgb->dgn-cons-1-dgb
  (implies (dgb-p dgb)
	   (equal (dgb->dgn (cons 1 dgb))
		  (+ 1 (ash (dgb->dgn dgb) 1)))))

(defthm dgop*dgop-loop-bmark
  (implies (and (natp dgn1)
		(natp dgn2)
		(natp dgn)
		(natp n)
		(< dgn (ash 1 n)))
	   (equal (ash (dgop*dgop-loop dgn1 dgn2 dgn n) 1)
		  (dgop*dgop-loop dgn1 dgn2 (ash dgn 1) (+ n 1))))
  :hints (("Goal" :in-theory (disable ash logxor natp evenp))))

(defthm logxor-acc1-acc2-expt-2-n
  (implies (and (natp acc1)
		(natp acc2)
		(natp n)
		(< acc1 (ash 1 n))
		(< acc2 (ash 1 n)))
	   (equal (logxor acc1 (+ acc2 (ash 1 n)))
		  (+ (ash 1 n) (logxor acc1 acc2))))
  :hints (("Goal"
	   :in-theory (disable logxor-m-ash-1-n)
	   :use ((:instance logxor-m-ash-1-n
			    (m acc2))
		 (:instance logxor-m-ash-1-n
			    (m (logxor acc1 acc2)))))))

(defthm dgop*dgop-loop-logxor
  (implies (and (natp dgn1)
		(natp dgn2)
		(natp acc1)
		(natp acc2)
		(natp n)
		(< acc1 (ash 1 n))
		(< acc2 (ash 1 n)))
	   (equal (dgop*dgop-loop dgn1 dgn2 (logxor acc1 acc2) n)
		  (logxor acc1 (dgop*dgop-loop dgn1 dgn2 acc2 n))))
  :hints (("Goal" :in-theory (disable ash logxor natp evenp)))
  :rule-classes nil)

(defthm dgop*dgop-loop-acc
  (implies (and (natp dgn1)
		(natp dgn2))
	   (equal (dgop*dgop-loop dgn1 dgn2 1 1)
		  (+ 1 (dgop*dgop-loop dgn1 dgn2 0 1))))
  :hints (("Goal" :in-theory (disable ash logxor evenp natp
				      dgop*dgop-loop-bmark)
	   :use ((:instance dgop*dgop-loop-bmark (dgn 0)
			    (n 0))
		 (:instance dgop*dgop-loop-logxor (acc1 1)
			    (acc2 0)
			    (n 1))))))

(defthm ash-dgop*dgop-1
  (implies (and (natp dgn1)
		(natp dgn2))
	   (equal (ash (dgop*dgop dgn1 dgn2) 1)
		  (dgop*dgop (ash dgn1 1)
			   (ash dgn2 1)))))

(defthm dgop*dgop-ash-1+ash
  (implies (and (natp dgn1)
		(natp dgn2))
	   (equal (dgop*dgop (ash dgn1 1) (+ 1 (ash dgn2 1)))
		  (+ 1 (ash (dgop*dgop dgn1 dgn2) 1)))))

(defthm dgop*dgop-1+ash
  (implies (and (natp dgn1)
		(natp dgn2))
	   (equal (dgop*dgop (+ 1 (ash dgn1 1)) dgn2)
		  (+ 1 (ash (dgop*dgop dgn1 dgn2) 1)))))
  
;;;----------------------------------------------------------------------------

(defthm dgop*dgop-dgb*dgb-aux
  (implies (and (dgb-p dgb1)
		(dgb-p dgb2))
	   (equal (dgb->dgn (dgb*dgb dgb1 dgb2))
		  (dgop*dgop (dgb->dgn dgb1)
			     (dgb->dgn dgb2))))
  :hints (("Goal" :in-theory (disable dgop*dgop ash logxor
				      dgb*dgb-cmp-ls-ls))))

(defthm dgop*dgop-dgb*dgb
  (implies (and (natp dgn1)
		(natp dgn2))
	   (equal (dgop*dgop dgn1 dgn2)
		  (dgb->dgn (dgb*dgb (dgn->dgb dgn1)
				     (dgn->dgb dgn2)))))
  :hints (("Goal" :in-theory (disable dgop*dgop ash logxor
				      dgb*dgb-cmp-ls-ls))))

(in-theory (disable dgop*dgop-dgb*dgb-aux))

;;;============================================================================

#|
(defun dgop-ext-int (ext-dgop)
  (declare (list ext-dgop))
  (when ext-dgop
    (unless (apply #'> ext-dgop)
      (error "In dgop-ext-int, the external dgop ~A is not decreasing."
             ext-dgop)))
  (the fixnum
       (apply #'logxor (mapcar #'(lambda (item)
                                   (declare (fixnum item))
                                   (the fixnum (ash 1 item)))
                               ext-dgop))))
|#

(defun dgop-ext-int (ext-dgop)
  (if (dgl-p ext-dgop)
      (if (endp ext-dgop)
	  0
	  (logxor (ash 1 (car ext-dgop))
		  (dgop-ext-int (cdr ext-dgop))))
      0))

#|
(defun dgop-int-ext (dgop)
  (declare (fixnum dgop))
;  (unless (typep dgop 'dgop)
;    (error "In dgop-int-ext, ~A is not a dgop." dgop))
  (the list
       (do ((dgop dgop (ash dgop -1))
            (rslt nil) ;; (rslt +empty-list+)
            (bmark 0 (1+ bmark)))
           ((zerop dgop) rslt)
           (declare (fixnum dgop bmark)
                    (list rslt))
           (when (oddp dgop)
             (push bmark rslt)))))
|#

(defun dgop-int-ext-do (dgop rslt bmark)
  (declare (xargs :measure (if (natp dgop) dgop 0)
		  :hints (("Goal" :in-theory (disable ash)))))
  (if (natp dgop)
      (if (zerop dgop)
	  rslt
	  (if (oddp dgop)
	      (dgop-int-ext-do (ash dgop -1) (cons bmark rslt) (1+ bmark))
	      (dgop-int-ext-do (ash dgop -1) rslt (1+ bmark))))
      nil))

(defun dgop-int-ext (dgop)
  (if (natp dgop)
      (dgop-int-ext-do dgop nil 0)
      nil))

;;;============================================================================

(encapsulate
 ()

 (local
  (defthm 1+ls-dgop-int-ext-do
    (implies (and (natp dgn)
		  (dgl-p (cons bmark rsl)))
	     (equal (1+ls (dgop-int-ext-do dgn rsl bmark))
		    (dgop-int-ext-do dgn (1+ls rsl) (1+ bmark))))))

 (local
  (defthm append-dgop-int-ext-do
    (implies (and (natp dgn)
		  (dgl-p (cons bmark (append rsl1 rsl2))))
	     (equal (append (dgop-int-ext-do dgn rsl1 bmark) rsl2)
		    (dgop-int-ext-do dgn (append rsl1 rsl2) bmark)))))

 (defthm dgop-int-ext-dgb->dgl-dgn->dgb
   (implies (natp dgn)
	    (equal (dgop-int-ext dgn)
		   (dgb->dgl (dgn->dgb dgn))))
   :rule-classes :definition)

 )
  
;;;============================================================================

(encapsulate
 ()

 (local
  (defthm |1-1+n|
    (implies (natp n)
	     (equal (+ 1 -1 n) n))))

 (local
  (defthm dgb->dgn-dgb-pos
    (implies (natp n)
	     (equal (dgb->dgn (dgb-pos n))
		    (ash 1 n)))))

 (local
  (defthm dgb->dgn-dgb-app
    (implies (and (dgb-p dgb1)
		  (dgb-p dgb2)
		  (dgb< dgb1 dgb2))
	     (equal (dgb->dgn (dgb-app dgb1 dgb2))
		    (logxor (dgb->dgn dgb1) (dgb->dgn dgb2))))))

 (local
  (defthm natp-dgop-ext-int
    (implies (dgl-p dgl)
	     (natp (dgop-ext-int dgl)))))

 (defthm dgop-ext-int-dgb->dgn-dgl->dgb
   (implies (dgl-p dgl)
	    (equal (dgop-ext-int dgl)
		   (dgb->dgn (dgl->dgb dgl))))
   :rule-classes :definition)

 )

;;;============================================================================

(defthm dgop*dgop-cmp-ls-ls
  (implies (and (natp dgn1)
                (natp dgn2))
           (equal (dgop*dgop dgn1 dgn2)
                  (dgop-ext-int (cmp-ls-ls (dgop-int-ext dgn1)
					   (dgop-int-ext dgn2)))))
  :hints (("Goal" :in-theory (disable dgop*dgop))))

;;;============================================================================

(defthm dgop*dgop-property
  (implies (and (natp dgop)
		(natp i)
		(natp j)
		(<= i j))
           (equal (dgop*dgop (dgop-ext-int (list (+ 1 j)))
                             (dgop*dgop (dgop-ext-int (list i))
					dgop))
                  (dgop*dgop (dgop-ext-int (list i))
                             (dgop*dgop (dgop-ext-int (list j))
					dgop))))
  :hints (("Goal"
	   :in-theory (disable dgop*dgop 
			       dgl->dgb
			       cmp-s-ls-property
			       cmp-ls-ls-recursive
			       dgb*dgb-cmp-s-ls))))

;;;============================================================================

(defthm dgop*dgop-associativity
  (implies (and (natp dgop1)
		(natp dgop2)
		(natp dgop3))
	   (equal (dgop*dgop (dgop*dgop dgop1 dgop2) dgop3)
		  (dgop*dgop dgop1 (dgop*dgop dgop2 dgop3))))
  :hints (("Goal" :in-theory (disable dgop*dgop))))

;;;============================================================================
